p:FinProbSpace, F:(Outcome), q:. (x:Outcome. q  F(x))  q  weighted-sum(p;F) 

latex

Definitions	t  T, x:AB(x), x:A. B(x), b, , ||as||, #$n, {i..j}, r  s, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , (x  l), Void, x:A.B(x), Top, a < b, type List, S  T, null(as), Type, x. t(x), xL. P(x), x:A  B(x), l[i], a  j < b. E(j), s = t, f(a), , Outcome, FinProbSpace, x.A(x), True, T, SqStable(P), x,y:A//B(x;y), a  b, suptype(S; T), weighted-sum(p;F), <a, b>
Lemmas	ws-constant, squash wf, true wf, weighted-sum wf2, p-outcome wf, sq stable from decidable, decidable qle, qsum wf, select wf, l all wf2, qle wf, int inc rationals, not wf, assert wf, null wf3, top wf, ws-monotone, l member wf, int seg wf, length wf1, rationals wf